package com.ecnu.codelearn.software_analysis;

import org.apache.commons.lang3.StringUtils;

import java.io.Serializable;
import java.util.List;

/**
 * Created by cao_peisheng@jiuyv.com on 2021/4/30 14:05
 * @author caopeisheng
 */
public class FirstOrderLogic implements Serializable {
    /**
     * 一阶逻辑公式所执行的语句片段
     */
    private String programSegment;
    /**
     * 一阶逻辑公式中改变的变量（赋值的情况才有）
     */
    private String variablesChanged;
    /**
     * 入口标记
     */
    private String inMark;
    /**
     * 出口标记
     */
    private String outMark;
    /**
     * 子程序一阶逻辑入口标记（并发时使用）
     */
    private List<String> subInMarkList;
    /**
     * 子程序一阶逻辑出口标记（并发时使用）
     */
    private List<String> subOutMarkList;

    /**
     * 拼好的一阶逻辑公式的字符串
     */
    private String firstOrderLogicStr;

    private String turn;

    public FirstOrderLogic() {
    }

    public FirstOrderLogic(String programSegment, String variablesChanged, String inMark, String outMark) {
        this.programSegment = programSegment;
        this.variablesChanged = variablesChanged;
        this.inMark = inMark;
        this.outMark = outMark;
    }

    public FirstOrderLogic(String programSegment, String variablesChanged, String inMark, String outMark, List<String> subInMarkList, List<String> subOutMarkList) {
        this.programSegment = programSegment;
        this.variablesChanged = variablesChanged;
        this.inMark = inMark;
        this.outMark = outMark;
        this.subInMarkList = subInMarkList;
        this.subOutMarkList = subOutMarkList;
    }

    public String getProgramSegment() {
        return programSegment;
    }

    public void setProgramSegment(String programSegment) {
        this.programSegment = programSegment;
    }

    public String getVariablesChanged() {
        return variablesChanged;
    }

    public void setVariablesChanged(String variablesChanged) {
        this.variablesChanged = variablesChanged;
    }

    public String getInMark() {
        return inMark;
    }

    public void setInMark(String inMark) {
        this.inMark = inMark;
    }

    public String getOutMark() {
        return outMark;
    }

    public void setOutMark(String outMark) {
        this.outMark = outMark;
    }

    public List<String> getSubInMarkList() {
        return subInMarkList;
    }

    public void setSubInMarkList(List<String> subInMarkList) {
        this.subInMarkList = subInMarkList;
    }

    public List<String> getSubOutMarkList() {
        return subOutMarkList;
    }

    public void setSubOutMarkList(List<String> subOutMarkList) {
        this.subOutMarkList = subOutMarkList;
    }

    public String getFirstOrderLogicStr() {
        String result = "";
        if (StringUtils.isNotBlank(inMark)) {
            result += "pc=" + inMark;
        }
        if (StringUtils.isNotBlank(outMark)) {
            if (result.length() > 0) {
                result += " ^ ";
            }
            result += "pc'=" + outMark;
        }
        if (subInMarkList != null && subInMarkList.size() > 0) {
            for (int i = 0; i < subInMarkList.size(); i++) {
                if (StringUtils.isNotBlank(subInMarkList.get(i))) {
                    if (result.length() > 0) {
                        result += " ^ ";
                    }
                    result += "pc"+i+"=" + subInMarkList.get(i);
                }
            }
        }
        if (subOutMarkList != null && subOutMarkList.size() > 0) {
            for (int i = 0; i < subOutMarkList.size(); i++) {
                if (StringUtils.isNotBlank(subOutMarkList.get(i))) {
                    if (result.length() > 0) {
                        result += " ^ ";
                    }
                    result += "pc"+i+"'=" + subOutMarkList.get(i);
                }
            }
        }
        if (StringUtils.isNotBlank(variablesChanged)) {
            if (result.length() > 0) {
                result += " ^ ";
            }
            result += "same(V/{" + variablesChanged + "})";
        }
        if (StringUtils.isNotBlank(programSegment)) {
            if (result.length() > 0) {
                result += " ^ ";
            }
            result += programSegment;
        }
        return result;
    }

    public void setFirstOrderLogicStr(String firstOrderLogicStr) {
        this.firstOrderLogicStr = firstOrderLogicStr;
    }

    public String getTurn() {
        return turn;
    }

    public void setTurn(String turn) {
        this.turn = turn;
    }

    @Override
    public String toString() {
        return "FirstOrderLogic{" +
                "programSegment='" + programSegment + '\'' +
                ", variablesChanged='" + variablesChanged + '\'' +
                ", inMark='" + inMark + '\'' +
                ", outMark='" + outMark + '\'' +
                ", subInMarkList=" + subInMarkList +
                ", subOutMarkList=" + subOutMarkList +
//                ", firstOrderLogicStr='" + getFirstOrderLogicStr() + '\'' +
                ", turn='" + turn + '\'' +
                '}';
    }
}
